\chapter{Rabbit Approach}
\label{ch:Approach}

This chapter explain Rabbit's idea to find race conditions, firstly we
introduce Rabbi with an illustrative example and after that presents more
details about Rabbit algoritm.

\Comment{
Concurrent errors are notably easy to introduce and difficult to find,
specially in programs that follow a shared-memory programming model.
In such model, executing threads communicate by reading and updating a
shared space in memory.  Programmers need to use some locking
mechanism (e.g., monitors or semaphores) to protect access to data,
i.e., to prevent different threads from reading or writing data
inconsistently.  The undisciplined use of locks can result in blocking
(e.g., deadlocks), lack of global progress (livelocks) and incorrect
state mutation (data races).
}


\section{Illustrative Example}
\label{sec:example}

Figure~\ref{fig:example:transfer} shows a fragment of a Java class
implementing a bank account that contains a data race.  We illustrate
how the \jpf{} model checker in standard mode performs to find this
error and then how \jpf{} in \tname{} mode performs.  The
class \CodeIn{Account} has one field to store the amount available in
the account and a method to transfer money between accounts.  The
method
\CodeIn{transfer} withdraws money from the target account object
(denoted by reference \CodeIn{this}) and deposits money into the
account object passed as parameter.  Note the use of the modifier
\CodeIn{synchronized} in the declaration of \CodeIn{transfer}.  It
has the effect of setting the target account object (i.e.,
\CodeIn{this}) as the \emph{monitor} for the method body; hence
blocking any thread that attempts to execute code that is also
protected by this monitor~\citep{arnold00:java}.\Comment{ The semantics
of Java monitors is defined elsewhere.}  Unfortunately, the protection
used in this example is not sufficient to prevent race.  The figure
shows a scenario where two distinct threads make calls to method
\CodeIn{transfer} on account objects \CodeIn{acc1} and \CodeIn{acc2}.
One thread transfers money from \CodeIn{acc1} to \CodeIn{acc2} and the
other does the opposite.  The problem in this example is that each
thread \emph{acquires a different monitor} to protect its critical
region.  The first thread acquires monitor
\CodeIn{acc1} and the second acquires monitor \CodeIn{acc2}.  As such
no synchronization is in effect; any interleaving is
possible\Comment{\footnote{This includes interleavings that violate
sequential consistency~\citep{manson-etal-2005}.}}.


\lstset{escapeinside={\%*}{*)}}
\subfiguretopcapfalse
\begin{figure}[t]
\centering
\begin{small}
\subfigure[Fragment of \texttt{Account} subject.]{
\lstinputlisting[language=java,
\Comment{numbers=left,numbersep=1pt,}basicstyle=\tiny]{Account.java}
\label{fig:example:transfer}
}\vspace{3ex}
\subfigure[Racy scheduling.]{
\includegraphics[scale=0.5]{chapters/approach/transfer_race.pdf}
\label{fig:example:race}
}\vspace{3ex}
\subfigure[\tname{} warning (running on top of JPF).]{
\lstinputlisting[language=java,
\Comment{numbers=left,numbersep=1pt,}basicstyle=\tiny]{RabbitReport.txt}
\label{fig:output}
}
\caption{Example of data race due to improper synchronization.}
\end{small}
\figtabsep{}
%  \vspace{-2ex}
\end{figure}







Figure~\ref{fig:example:race} shows one particular scenario of race.
To facilitate illustration, we use a thread-local artificial
variable \CodeIn{tmp} to store values read from object fields.  The
second thread reads the values of \CodeIn{acc2.amount} first, then the
first thread executes to completion, and finally the second thread
resumes using the value stored in \CodeIn{tmp}, which is incorrect as
it differs from \CodeIn{acc2.amount}'s current value.  Assuming that
both accounts store 100 in field \CodeIn{amount} at the beginning of
execution, the improper synchronization will result in an incorrect
modification of \CodeIn{acc2.amount} to 97 instead of 107.  This
violates the state assertion in the main method as the sum of the
account balances resulted in 190 instead of 200, as expected.

\vspace{1ex}\noindent\textbf{Java PathFinder (JPF).}
\Comment{It is possible that the user does not realize a problematic scheduling
in this example.}  Software model checkers have been proposed to
systematically explore the space of thread interleavings to find
errors like this.  Java PathFinder (JPF) is one explicit-state model
checker for Java programs.  It implements a\Comment{n extensible} Java
Virtual Machine (VM), equipped with state storage and backtracking
capabilities, different search strategies, and listeners for
monitoring and influencing the search.  For this example, JPF explores
all possible thread interleavings (modulo its space reduction
strategies) reachable from
\CodeIn{Account}'s main method and takes only $\sim$1s to find the
error above.  Unfortunately, the state-space reachable from the tests
of arbitrary concurrent programs can be significantly larger than this
one~\citep{gligoricEtAl-icst2010,jagannathEtAl2011}.  To simulate this,
we considered a modified version of this main method involving 7
threads and other methods from \CodeIn{Account} such
as \CodeIn{deposit} and \CodeIn{withdraw}; for such modified
configuration, JPF took 3m39s to report the same error (see
Figure~\ref{tab:results}).

\Comment{
It finds all warnings reported in the course of 1 minute
in the first 5 seconds (see Table~\ref{table:results}). \tname{} uses
the monitoring infra-structure of JPF to compute the warnings.}

%% JavaPathfinder v6.0 - (C) RIACS/NASA Ames Research Center
%% Elapsed Time 5 seconds

%% \Fix{os tres erros são reflexos do acesso desprotegido ao mesmo ponto
%%   do programa, contudo o race poderia se manifestar na combinação
%%   entre o metodo transfer e os metodos (deposite, tranfer, e
%%   withdraw).Então o rabbit indica os seguintes pares de acesso que
%%   podem causar o erro tranfer, deposite; tranfer, withdraw; tranfer,
%%   tranfer }

%\lstset{escapeinside={\%*}{*)}}
\subfiguretopcapfalse
\begin{figure}[t]
\centering
\begin{small}

\subfigure[\label{fig:approach}Conceptual illustration
of \tname{}.]{ \includegraphics[scale=0.6]{chapters/approach/approach.pdf}
}\vspace{3ex}

\subfigure[\label{fig:rabbit}Non-racy scheduling
for \texttt{Account} example, but \tname{} produces a correct
warning
reported.]{ \includegraphics[scale=0.6]{chapters/approach/transfer_ok.pdf} }

\end{small} \caption{Illustration using \emph{one}
schedule.}  \figtabsep{}
\end{figure}

\vspace{1ex}\noindent\textbf{\tname{}.}  \tname{} reports the corresponding warning in less than
5 seconds for this larger configuration, involving 7 threads.  It
reports a total of 3 different but positive warnings all of which are
related to the same problem: the improper synchronization in
method \CodeIn{transfer}.  \tname{} reports 2 additional conflicts
involving accesses made within transfer and other methods
of \CodeIn{Account} that also access the field \CodeIn{amount}, namely
the \CodeIn{withdraw} and
\CodeIn{deposit} methods.

Figure~\ref{fig:approach} illustrates the \tname{} approach at the
conceptual level.  The figure shows with vertical lines two executing
threads.  The small rectangles over the line segments denote context
switches and the line segments denote straight-line execution within
the individual threads\Comment{ according to an interleaving
semantics}.  \tname{} signals the presence of potential conflicts
during the search by relating previously observed and current memory
accesses.  This is possible because \tname{} is able to relate
identical objects across the state-space exploration; this is key
because there is no guarantee that the id assigned by the model
checker to one new object will be preserved across different
exploration paths (see Section~\ref{sec:objectIDs}).  The note inside
the box from Figure~\ref{fig:approach} characterizes the scenario of a
potential race.  It is important to note that even though this scenario
shows only one schedule of the program under test (for space
reasons), \tname{} observes and relates memory accesses across
multiple schedules.  It is also important to note that reported warnings are
not necessarily conflicting as events $r_1$ and $w_1$ from
Figure~\ref{fig:approach} could be causally related.  For example, the
semantics of the program could denote that the event $w_1$ always
follows from $r_1$; therefore, it would not be possible to construct a
scenario where these events compete for the same resources.  However,
we conjecture that \tname{} is precise in practice even ignoring the
possibility of general causalities.  The \emph{precision} of \tname{}
originates from its ability to: (i) dynamically relate object ids from
potentially distinct schedules\Comment{(which also enables field
sensitivity)}, (ii) detect simple causal relationships, and (iii)
detect (and remove) similar warning reports.

The \emph{efficiency} of \tname{} originates from the observation that
memory accesses are typically covered much sooner than the actual
race.  For example, Figure~\ref{fig:rabbit} illustrates a safe
scheduling of two threads that a model checker may explore.  For this
particular case, \tname{} needs only one schedule to report a positive
warning.  Note that this schedule does \emph{not} actually manifest a
race: when the second thread reads from \CodeIn{acc1.amount} the first
thread already left its critical region.  In this case, \tname{}
predicts that a racy scheduling could be created as the same field
from the same object was accessed (to read and to write) from
different threads using disjoint lock sets
\{acc1\} and \{acc2\}.  \Comment{Important to note that \tname{}
only relates accesses to the same memory location; therefore its
inability to detect general causalities is bound to those accesses.}

\vspace{1ex}\noindent\textbf{\tname{}'s output.}  Figure~\ref{fig:output} shows a fragment of the
output of \tname{} for the main method from
Figure~\ref{fig:example:transfer}.\Comment{ This is a compacted
version of the output that filters the potential conflicts.}  It
indicates that there is a potential race in the access of field
\CodeIn{amount} through one instance of \CodeIn{Account}.\Comment{ Lines
beginning with \CodeIn{read} and \CodeIn{write} correspond to field
accesses.}  Note that the output of \tname{} is per object and per
field and appears in tree format to indicate to which object and field
an access is associated.  Each line in leaf position shows if the
access was a read or write, the thread that originated the access,
the method and line of the access, and a list of locksets.  Each
distinct lockset observed across field accesses appears inside
parentheses\Comment{; the numbers inside parentheses indicate the
different locks~\footnote{\tname{} operates at bytecode level and
deals with Java monitors; other locking mechanisms such
as \CodeIn{Lock}s are treated as syntactic sugar.}}.  For example,
the report from Figure~\ref{fig:output} shows that two different
threads access field \CodeIn{amount} on \CodeIn{Account} object 415
using inconsistent locksets (i.e., disjoint sets of locks).  While
thread ``Thread-4'' holds locks 408 and 415 when reading
field \CodeIn{amount}, thread ``Thread-3'' writes to the same field
using the lock 401.  This warning is in fact positive and looks
similar to the (actual) race report from \jpf{}.

\Comment{
Note the user still needs to identify and fix the
fault (either in JPF or \tname{}).}


% LocalWords:  livelocks escapeinside numbersep basicstyle acc tmp PathFinder
% LocalWords:  interleavings JPF VM locksets lockset bytecode java pt txt etal
% LocalWords:  RabbitReport icst JavaPathfinder RIACS os tres
